Хорновская выполнимость

КНФ называется **хорновской**, если каждый её клоз содержит не более одной переменной без отрицания. Пример: $F = (\bar{a} \lor b \lor \bar{c}) \land (\bar{b} \lor \bar{d}) \land (a) \land (\bar{a} \lor d)$

**HornSAT** — частный случай задачи SAT, в котором рассматриваются только хорновские КНФ. Для данной задачи существуют линейные алгоритмы решения.

Задача HornSAT может быть решена за время $O(m)$, где $m$ — суммарное число литералов в формуле.

Применим метод распространения зависимостей и вычислим $UP(F)$ за время $O(m)$. Если получено значение из $\{0, 1\}$, то ответ найден. Иначе каждый оставшийся клоз содержит не менее двух литералов. В силу определения хорновской КНФ, в каждом таком клозе обязательно присутствует хотя бы одна переменная с отрицанием $\bar{x}$. Присвоим всем оставшимся переменным значение $0$. В этом случае в каждом клозе будет хотя бы один истинный литерал $\Rightarrow UP(F)$ выполнима $\Rightarrow F$ выполнима. $\square$